(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r9 Real)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const v21 Bool)
(declare-const v25 Bool)
(declare-const v32 Bool)
(declare-const v33 Bool)
(assert (or v32 v33 (distinct 44880.0 43.809 r13 r11) (and v3 v21 v2 v25 v18 (distinct r0 (* r13 543079375.0 r12 r12) r3) v4 (<= 543079375.0 r0 r9) v0) v32))
(assert (or v32))
(check-sat)
